T:Type, l1,l2:(T List), x:T.
iseg(T; l1; append(l2; cons(x; [])))  (iseg(T; l1; l2)  (l1 = append(l2; cons(x; [])))) 

latex

Definitions	P  Q, x:A. B(x), t  T, x:A. B(x), iseg(T; l1; l2), guard(T), P  Q, append(as; bs), prop{i:l}, ||as||, P  Q, P  Q, P  Q, True, T, False, b
Lemmas	iseg weakening, cons iseg, iseg nil, squash wf, true wf, iff functionality wrt iff, iseg append iff, length wf1, append wf, iseg wf